Nuprl Lemma : rng_nexp_unroll
13,42
postcript
pdf
r
:Rng,
n
:
,
e
:|
r
|. (
e
r
n
) = ((
e
r
(
n
- 1)) *
e
)
|
r
|
latex
Up
rings
1
Definitions of Statement
Rng
,
r
xmn
,
e
r
n
Definitions
t
T
,
x
f
y
,
x
:
A
.
B
(
x
)
,
t
.2
,
t
.1
,
r
xmn
,
*
,
|
g
|
,
e
r
n
Lemmas
rng
wf
,
mul
mon
of
rng
wf
c
,
mon
nat
op
unroll
origin
r:Rng, n:
, e:|r|. (e 
r n) = ((e r (n - 1)) * e) 
|r| r:Rng, n:, e:|r|. (e r n) = ((e r (n - 1)) * e) |r| 
xmnr n Tx:A. B(x)xmnr n